Nuprl Lemma : append_back_nil
2,24
postcript
pdf
T
:Type,
as
:
T
List. (
as
@ nil) =
as
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
T:Type, as:T List. (as @ nil) = as T:Type, as:T List. (as @ nil) = as 
Tx:A. B(x)